Introduce named simplify databases, a head-symbol filter, and proof-local
control over which user-reduction rules `simplify`/`cbv` apply. These are
all expressed through one `hint` clause, used in three places: after a
`simplify`/`cbv` tactic, as a standalone `hint` command, and in the
`with hint … (…)` scoped wrapper.

Theory-level declarations register lemmas into a database (unchanged):

    hint simplify {lemma}+ .             (* default database *)
    hint simplify in {db} : {lemma}+ .   (* named database   *)

On the `simplify`/`cbv` tactics, a `hint` clause chooses the rules for
that call. The clause is `hint` followed by items disambiguated by their
delimiter -- a bare name is a database, `[…]` holds operators, `{…}` holds
lemmas:

    simplify hint d1 d2                  (* consult exactly d1, d2     *)
    simplify hint +d1 -d2                (* +/- a db on the active set *)
    simplify hint +[f g]                 (* restrict user rules to f,g *)
    simplify hint {L}                    (* add lemma L for this call  *)
    cbv hint d1 {M}

The database part is either an unsigned selection (replace) or signed +/-
deltas (on the active set), never both; at most one head filter is
allowed; and lemma sets `{…}` are add-only -- a clause never removes
lemmas from a database (use the head filter to restrict which rules
apply).

The same clause, written as a standalone command, changes the proof state
persistently:

    hint +d1 -d2 .                       (* activate / deactivate DBs  *)
    hint {L} .                           (* add local lemmas           *)
    hint d1 d2 .                         (* set default databases      *)
    hint +[f g] .                        (* set default head filter    *)
    hint clear [ {db} ] .                (* clear local additions      *)
    hint clear default .                 (* clear proof-local defaults *)

and as a scoped wrapper, in effect only for the wrapped tactic and
restored on the resulting subgoals:

    with hint {clause} ( {tactic} ) .

Implementation: the proof-local simplify context lives in a new
EcSimplifyContext module (extracted from EcEnv); it is threaded through
proof goals so the active DB set, added lemmas, default database, and
head filter propagate across subgoals and are consulted by `simplify` and
`cbv`. Reduction storage and simplify-hint printing support named
databases and head filtering.

Document the syntax in doc/tactics/hint-simplify.rst and add regression
tests (tests/hint_simplify_db.ec, tests/local_hint_simplify.ec,
tests/simplify_head_filter.ec).